Issue2059.agda:32,1-24
obvious  is not a legal rewrite rule, since the following variables are not bound by the left hand side:  p
when checking the pragma REWRITE obvious
